Isabelle-HoTT/ex/HoTT book, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 add ROOT file 2018-09-18T14:52:08+00:00 Lars Hupel 2018-09-18T14:52:08+00:00 f07e0e2349a222130209ada9c029eea3d1fe8144 






Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0!
2018-09-18T09:38:54+00:00

Josh Chen

2018-09-18T09:38:54+00:00

6857e783fa5cb91f058be322a18fb9ea583f2aad












Should write the correct rule for Ord_leq_min. Another exercise.
2018-08-29T22:51:48+00:00

Josh Chen

2018-08-29T22:51:48+00:00

2a2e8e46e0de6f99154a9421f75ae802557f22c7












Regrouping type rules
2018-08-18T19:28:21+00:00

Josh Chen

2018-08-18T19:28:21+00:00

e1be5f97bb2a42b3179bc24b118d69af137f8e5d












Misc formatting
2018-08-18T12:34:08+00:00

Josh Chen

2018-08-18T12:34:08+00:00

41f13f91d023e497d9b35e7a958a961aa0c7a5e5












Some comments and reorganization
2018-08-16T14:28:50+00:00

Josh Chen

2018-08-16T14:28:50+00:00

d8699451025a3bd5e8955e07fa879ed248418949